;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Mtradeincrease.lisp")
(require "Mstock-retrieval.lisp")
(require "Mio.lisp")
(require "DataGenerators.lisp")

(module Ttradeincrease
  (import Itradeincrease)
  (import Itree)
  ;(import Ii/o)
  
; check-expect tests  
  (include-book "list-utilities" :dir :teachpacks)
  (include-book "io-utilities" :dir :teachpacks)
  (include-book "testing" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks)
  
  ;(check-expect (tradeincrease "AA" "20100406" "20100406" (read-stocks-file "test.txt")) '("AA" 0))
  ;(check-expect (tradeincrease-query "AA" "20100406" "20100406" (read-stocks-file "test.txt")) "AA: 0%")
  
  
  ; random ticker
  (defrandom random-ticker ()
    (random-string))
  
  ; random date
  (defrandom random-date ()
    (int->str (random-between 19000101 20990101)))
  
  ; random stock entry from the file, includes the date
  (defrandom random-stocks-file-line ()
    (list (random-date) (random-ticker) (random-natural) (random-natural)
          (random-natural) (random-natural) (random-natural)))
  
  ; random stock entry from within the sub-trees in the AVL tree
  (defrandom random-stock-entry ()
   (list (random-ticker) (random-natural) (random-natural)
         (random-natural) (random-natural) (random-natural)))
                                                             
  
  ; random tree - constructs an AVL tree
  ; given a list of stock file lines
  ; using insert-record
  (defun generate-tree (stocks tree)
    (if (consp stocks)
        (let* ((stock (car stocks))
           (date (car stock))
           (ticker (cadr stock))
           (opening-price (caddr stock))
           (highest-price (cadddr stock))
           (lowest-price (car (cddddr stock)))
           (closing-price (car (cdr (cddddr stock))))
           (num-traded (car (cdr (cdr (cddddr stock)))))
           (datalist (list opening-price highest-price lowest-price closing-price num-traded)))
      (if (equal (avl-retrieve tree date) nil)
          (generate-tree (cdr stocks) (avl-insert tree date (avl-insert (empty-tree) ticker datalist))) ; if the given date doesn't exist, create it in the tree
          (generate-tree (cdr stocks) (avl-insert tree date (avl-insert (cdr (avl-retrieve tree date)) ticker datalist)))))
        tree))
  
  ; random tree
  (defrandom random-stock-tree ()
    (generate-tree (random-list-of (random-stocks-file-line)) (empty-tree)))
  
  ;tests that tradeincrease returns a list 
  (defproperty tradeincrease-returns-list-prp
    (ticker :value (random-string) 
     start  :value (random-date)
     end    :value (random-date)
     :where (<= (str->int end) (str->int start))
     tree   :value (random-stock-tree))
    (equal t (listp (tradeincrease ticker start end tree))))
 
   ;tests that the tradeincrease-query function always returns a string
  (defproperty tradeincrease-query-returns-string-prp
    (start   :value (random-date)
     end     :value (random-date)
             :where (<= (str->int end) (str->int start))
     tickers :value (random-list-of (random-ticker))
     tree    :value (random-stock-tree))
    (equal t (stringp (tradeincrease-query start end tickers tree))))
  )

(link RTtradeincrease (Mtree Mstockretrieval Mhelpers DataGenerators Mtradeincrease Ttradeincrease))
(invoke RTtradeincrease)
  
